Skip to content

feat(Analysis/ODE): add discrete Grönwall inequality#34709

Open
dennj wants to merge 1 commit intoleanprover-community:masterfrom
dennj:feat/discrete-gronwall
Open

feat(Analysis/ODE): add discrete Grönwall inequality#34709
dennj wants to merge 1 commit intoleanprover-community:masterfrom
dennj:feat/discrete-gronwall

Conversation

@dennj
Copy link
Copy Markdown
Contributor

@dennj dennj commented Feb 2, 2026 •
edited
Loading

Summary

Add discrete Grönwall inequality to Mathlib/Analysis/ODE/DiscreteGronwall.lean

Provides bounds for recurrence inequalities of the form u(n+1) ≤ c(n) * u(n) + b(n)

Main results

  • discrete_gronwall_prod_general: Product form working over any linearly ordered commutative ring
  • prod_one_add_Ico_mono: Auxiliary lemma for product comparisons over subintervals
  • discrete_gronwall: Classical exponential bound u(n) ≤ (u(n₀) + ∑ b(k)) * exp(∑ c(i)) (ℝ-specific)
  • discrete_gronwall_Ico: Uniform bound over a finite interval (ℝ-specific)

Related work

Complements the continuous Grönwall inequality in Mathlib.Analysis.ODE.Gronwall

References

  • Grönwall, T. H. (1919). "Note on the derivatives with respect to a parameter of the solutions of a system of differential equations". Annals of Mathematics, 20(4), 292–296.

This is human-made PR with AI help in golfing proof and documenting the code.

@github-actions github-actions Bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus) labels Feb 2, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Feb 2, 2026 •
edited
Loading

PR summary 977f84bd6e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.ODE.DiscreteGronwall (new file) 1920

Declarations diff

+ discrete_gronwall
+ discrete_gronwall_Ico
+ discrete_gronwall_prod_general

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib-triage mathlib-triage Bot assigned j-loreaux and unassigned ADedecker Mar 11, 2026
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Mar 16, 2026

Hello from triage! My impression is that this PR was generated with substantial help from LLM. Can you comment on this, please? Per our AI policy, also mention this in the PR description.

@grunweg grunweg added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 16, 2026
j-loreaux
j-loreaux reviewed Mar 20, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Long story short: grind is your friend.

Can you please answer the question about whether this PR is generated or assisted by AI?

Comment thread Mathlib/Analysis/ODE/DiscreteGronwall.lean Outdated
Comment thread Mathlib/Analysis/ODE/DiscreteGronwall.lean Outdated
Comment thread Mathlib/Analysis/ODE/DiscreteGronwall.lean Outdated
Comment thread Mathlib/Analysis/ODE/DiscreteGronwall.lean Outdated
Comment thread Mathlib/Analysis/ODE/DiscreteGronwall.lean Outdated
Comment thread Mathlib/Analysis/ODE/DiscreteGronwall.lean Outdated
Comment thread Mathlib/Analysis/ODE/DiscreteGronwall.lean Outdated
Comment thread Mathlib/Analysis/ODE/DiscreteGronwall.lean Outdated
Comment thread Mathlib/Analysis/ODE/DiscreteGronwall.lean Outdated
@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 20, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 20, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts Bot commented Mar 20, 2026

This pull request has conflicts, please merge master and resolve them.

@euprunin
Copy link
Copy Markdown
Contributor

euprunin commented Apr 11, 2026 •
edited
Loading

@dennj

Are you familiar with the merely-true project (https://github.com/merely-true/merely-true)? It's intended as a playground for LLM-generated mathematics, with very permissive contribution guidelines.

I'm not a Mathlib reviewer or maintainer, so I don't speak for the project, but I thought I'd mention it as a potentially interesting place for work like this (independently of how this PR is evaluated here).

@dennj dennj force-pushed the feat/discrete-gronwall branch from 5439f72 to 1015cc2 Compare April 27, 2026 00:20
@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 27, 2026
@dennj dennj force-pushed the feat/discrete-gronwall branch from 1015cc2 to 099dcf6 Compare April 27, 2026 00:25
@dennj
Copy link
Copy Markdown
Contributor Author

dennj commented Apr 27, 2026

-awaiting-author

I applied the suggestions in the comments and did some golfing

@github-actions github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 27, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

Assignees

@j-loreaux j-loreaux

Labels

LLM-generated PRs with substantial input from LLMs - review accordingly new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@dennj @grunweg @euprunin @j-loreaux @ADedecker